#ifndef BASIC_SET_OPERATIONS_HH_
#define BASIC_SET_OPERATIONS_HH_

///
/// \file basic_set_operations.hh
/// \brief definitions of low level bdd operators.
/// \author Coddy Levi, Sylvain Lobry
/// \version 1.0
///
///
///

#include <bdd.h>

#include "Model.hh"

///
/// \brief Compute the bdd composed of the predecessors, as defined in the
/// kripke structure, of a bdd.
///
/// \param[in]	a The bdd on which to compute predecessors
/// \param[in]	m The Model class describing the kripke structure.
/// \return	The resulting bdd
///
bdd compute_predecessors(bdd a, const Model& m);

///
/// \brief Compute the bdd composed of the successors, as defined in the
/// kripke structure, of a bdd.
///
/// \param[in]	a The bdd on which to compute successors
/// \param[in]	m The Model class describing the kripke structure.
/// \return	The resulting bdd
///
bdd compute_successors(bdd a, const Model& m);

///
/// \brief Compute the bdd representing the set of states validating
/// a set of variables (label)
///
/// \param[in]	var The bdd describing the set of variables
/// \param[in]	m The Model class describing the kripke structure.
/// \return	The resulting bdd
///
bdd compute_validating_states(bdd var, const Model& m);

///
/// \brief Compute the complementary bdd
///
/// \param[in]	a The bdd on which to compute the complementary
/// \param[in]	m The Model class describing the kripke structure.
/// \return	The resulting bdd
///
bdd compute_not(bdd a, const Model& m);

#endif
